$\forall$$A$:Type, $I$:MaInterface($A$), $i$:Id.
\\[0ex]($i$ $\in$ ma{-}interface{-}locs($I$))
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$ma{-}interface{-}loc($I$;$i$)))
\\[0ex]$\Rightarrow$ (ma{-}interface{-}conds($I$;$i$) $\in$ $k$:Knd fp$\rightarrow$ Void)